Termination of rewriting strategies : a generic approach
Identifieur interne : 005F28 ( Main/Exploration ); précédent : 005F27; suivant : 005F29Termination of rewriting strategies : a generic approach
Auteurs : Isabelle Gnaedig ; Hélène KirchnerSource :
English descriptors
- KwdEn :
Abstract
We propose a generic termination proof method for rewriting under strategies, based on an explicit induction on the termination property. Rewriting trees on ground terms are modelized by proof trees, generated by alternatively applying narrowing and abstracting steps. The induction principle is applied through the abstraction mechanism, where terms are replaced by variables representing any of their normal forms. The induction ordering is not given a priori, but defined with ordering constraints, incrementally set during the proof. The generic method is then instantiated for the innermost strategy, as an example.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 004370
- to stream Crin, to step Curation: 004370
- to stream Crin, to step Checkpoint: 000376
- to stream Main, to step Merge: 006151
- to stream Main, to step Curation: 005F28
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="292">Termination of rewriting strategies : a generic approach</title></titleStmt><publicationStmt><idno type="RBID">CRIN:gnaedig05b</idno><date when="2005" year="2005">2005</date><idno type="wicri:Area/Crin/Corpus">004370</idno><idno type="wicri:Area/Crin/Curation">004370</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">004370</idno><idno type="wicri:Area/Crin/Checkpoint">000376</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">000376</idno><idno type="wicri:Area/Main/Merge">006151</idno><idno type="wicri:Area/Main/Curation">005F28</idno><idno type="wicri:Area/Main/Exploration">005F28</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Termination of rewriting strategies : a generic approach</title><author><name sortKey="Gnaedig, Isabelle" sort="Gnaedig, Isabelle" uniqKey="Gnaedig I" first="Isabelle" last="Gnaedig">Isabelle Gnaedig</name></author><author><name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Hélène" last="Kirchner">Hélène Kirchner</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>abstraction</term><term>induction</term><term>innermost</term><term>local strategy</term><term>narrowing</term><term>ordering constraint</term><term>outermost</term><term>rewriting</term><term>strategy</term><term>termination</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="2492">We propose a generic termination proof method for rewriting under strategies, based on an explicit induction on the termination property. Rewriting trees on ground terms are modelized by proof trees, generated by alternatively applying narrowing and abstracting steps. The induction principle is applied through the abstraction mechanism, where terms are replaced by variables representing any of their normal forms. The induction ordering is not given a priori, but defined with ordering constraints, incrementally set during the proof. The generic method is then instantiated for the innermost strategy, as an example.</div></front></TEI><affiliations><list></list><tree><noCountry><name sortKey="Gnaedig, Isabelle" sort="Gnaedig, Isabelle" uniqKey="Gnaedig I" first="Isabelle" last="Gnaedig">Isabelle Gnaedig</name><name sortKey="Kirchner, Helene" sort="Kirchner, Helene" uniqKey="Kirchner H" first="Hélène" last="Kirchner">Hélène Kirchner</name></noCountry></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005F28 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005F28 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= CRIN:gnaedig05b
|texte= Termination of rewriting strategies : a generic approach
}}
| This area was generated with Dilib version V0.6.33. |  |